Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		eq(0,0)	→ true
2:		eq(0,s(X))	→ false
3:		eq(s(X),0)	→ false
4:		eq(s(X),s(Y))	→ eq(X,Y)
5:		rm(N,nil)	→ nil
6:		rm(N,add(M,X))	→ ifrm(eq(N,M),N,add(M,X))
7:		ifrm(true,N,add(M,X))	→ rm(N,X)
8:		ifrm(false,N,add(M,X))	→ add(M,rm(N,X))
9:		purge(nil)	→ nil
10:		purge(add(N,X))	→ add(N,purge(rm(N,X)))

There are 7 dependency pairs:


11:		EQ(s(X),s(Y))	→ EQ(X,Y)
12:		RM(N,add(M,X))	→ IFRM(eq(N,M),N,add(M,X))
13:		RM(N,add(M,X))	→ EQ(N,M)
14:		IFRM(true,N,add(M,X))	→ RM(N,X)
15:		IFRM(false,N,add(M,X))	→ RM(N,X)
16:		PURGE(add(N,X))	→ PURGE(rm(N,X))
17:		PURGE(add(N,X))	→ RM(N,X)

The approximated dependency graph contains 3 SCCs: {11}, {12,14,15} and {16}.

Consider the SCC {11}. There are no usable rules. By taking the AF π with π(EQ) = 1 together with the lexicographic path order with empty precedence, rule 11 is strictly decreasing.

Consider the SCC {12,14,15}. The usable rules are {1-4}. By taking the AF π with π(RM) = 2, π(IFRM) = 3, π(eq) = [ ] and π(add) = [2] together with the lexicographic path order with precedence eq ≻ false and eq ≻ true, the rules in {4,12} are weakly decreasing and the rules in {1-3,14,15} are strictly decreasing.

Consider the SCC {16}. The usable rules are {1-8}. By taking the AF π with π(PURGE) = 1, π(rm) = 2, π(ifrm) = 3, π(eq) = [ ] and π(add) = [2] together with the lexicographic path order with precedence eq ≻ false and eq ≻ true, the rules in {4-6,8} are weakly decreasing and the rules in {1-3,7,16} are strictly decreasing.

Hence the TRS is terminating.

Tyrolean Termination Tool (0.25 seconds) --- May 4, 2006